Make let rec build cyclic data, and compare it by bisimulation - #16

Follow-up to the cyclic `let rec` commit, and an audit rather than just its
loose ends: three of these were already wrong before that change.

Already stale:

- §5 said a Table's hash sorts its entries "by key per §6's generic total
  order". It sorts by the key's *digest*, deliberately - §6's cross-type
  ordering is not built, and a digest order is deterministic without it.
- §5 filed hashing, equality and ordering under one heading, which reads as
  though equality were hash-derived. It is structural: entries matched by key
  and compared pairwise. Only `File` compares through its digest, because §3
  defines a File's identity that way. Split into two bullets.
- §8 named the nesting budget's constant `MAX_EVAL_DEPTH`; it has been
  `MAX_NEST_DEPTH` in eval.odin all along.

Stale as of the cyclic `let rec` change:

- §10 stated as a general rule that `rec` "changes which scope the value is
  computed in, and nothing else". True for every shape but the one the same
  section now describes at length, so both the rule and the two consequence
  bullets under it are qualified where they are stated rather than silently
  contradicted further down.
- §10's mutual-recursion bullet explained the one-`rec`-over-a-Table idiom as
  entries being closures over the scope holding the name. That was the whole
  story when only functions could do it. The Table is now bound before its
  entries run and the entries are demanded, which is why the same spelling
  works for data; the closure property still explains why a later call
  resolves, but it is no longer what makes the binding work.
- §8 enumerates failure sources and numbers them, so a circular definition is
  added as the sixth, next to the fourth and before the paragraph that draws
  the conclusion from the list. It is distinguished from the nesting budget:
  detected and named, rather than noticed by running out of stack.
- §15 presented `sha256` as total. It has one gap that is this document's
  rather than an implementation's - a cyclic value, whose digest §6 has not
  settled the encoding of.

Every behavioural claim added here was run against `hb` first: entry order
affecting neither equality nor the digest, the circular-definition message,
`sha256` of a cycle, and an unbounded `let rec` reaching the nesting budget
rather than the circularity check.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

Two unequal Tables could compare equal. Found by testing the case the
original tests missed - cyclic values used as Table *keys*:

  let rec g { .a = { .tag = "a", .next = g.b }, .b = { .tag = "b", .next = g.a } };
  let rec h { .a = { .tag = "a", .next = h.b }, .b = { .tag = "b", .next = h.a } };
  let X { [g.a] = 1, [g.b] = 2, .z = g.a };
  let Y { [h.b] = 2, [h.a] = 1, .z = h.b };
  X == Y        // was true; `g.a == h.b` is false on its own

The bisimulation walk is optimistic: descending into a pair of Tables it
records "assume these two are equal" and compares their entries under that
assumption. Those assumptions are only justified if the descent succeeds.
The header comment claimed nothing needed rolling back because a mismatch
returns false and discards the lot - true of the value spine, where every
caller propagates a false immediately, and false of the one loop that does
not: matching a key scans candidates and keeps going after a failure.

So a failed key match left claims behind. Matching `g.a` against the
candidate `h.b` fails, but not before asserting g.a ~ h.b; the later `.z`
comparison of exactly that pair then short-circuited to true on it.

Key matching is a self-contained question about two subgraphs, so it no
longer shares the walk's state at all - table_find compares each candidate
through values_equal, which makes its own. Isolation costs only the chance to
reuse a valid assumption, and cannot lose an answer: an isolated comparison
re-derives whatever it needs and still terminates on its own back-edges. The
scalar path is untouched, since a Bisim is a stack struct whose map is only
created when two distinct Tables are first assumed equal - and comparing a
scalar key never gets that far.

Five regression tests, covering this and the other gaps the same audit turned
up: different-period cycles that genuinely differ, a cycle against a finite
unrolling, symmetry (the two operands are not handled alike - one is walked,
the other looked up in), and a cyclic value as a key at all.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>